Lemma exact_condition:
  forall P Q R: Prop, (P->Q) -> (Q->R) -> P -> R.
Proof.
  intros.
  exact(H0 (H H1)).
Qed.